-------------------------------- MODULE TraceMultiNodeReads -------------------------------
EXTENDS MultiNodeReads, Json, IOUtils, Sequences, SequencesExt

Stats == 
    PrintT(<<"VARIABLE l (TLCGet(0))", TLCGet(0)>>)

\* Trace validation has been designed for TLC running in default model-checking
\* mode, i.e., breadth-first search.
\* The property TraceMatched will be violated if TLC runs with more than a single worker.
\* TLC register 0 is used to hold the count of line numbers processed, so it can be checked
\* in the post-condition, which can only include constants and not state variables such as l.
ASSUME TLCGet("config").mode = "bfs" /\ TLCGet("config").worker = 1 /\ TLCSet(0, 0)

JsonFile ==
    IF "JSON" \in DOMAIN IOEnv THEN IOEnv.JSON ELSE "trace.ndjson"

JsonLog ==
    \* Deserialize the System log as a sequence of records from the log file.
    \* Run TLC from under the tla/ directory with:
    \* ./tlc.py --ccf-raft-trace ../build/consistency/trace.ndjson consistency/TraceMultiNodeReads.tla
    \* Traces can be generated by running ./tests.sh -VV -R consistency_trace_validation under build/
    \* The clients execute transactions sequentially, and so the log is ordered by tx
    ndJsonDeserialize(JsonFile)

VARIABLE l

TraceInit ==
    /\ l = 1
    /\ Init

logline ==
    JsonLog[l]

ToTxType ==
    "RwTxRequest" :> RwTxRequest @@
    "RwTxResponse" :>  RwTxResponse @@
    "TxStatusReceived" :> TxStatusReceived @@
    "RoTxRequest" :> RoTxRequest @@
    "RoTxResponse" :>  RoTxResponse

ToStatus ==
    "CommittedStatus" :> CommittedStatus @@
    "InvalidStatus" :>  InvalidStatus


IsEvent(e) ==
    \* Equals FALSE if we get past the end of the log, causing model checking to stop.
    /\ l \in 1..Len(JsonLog)
    /\ logline.action = e
    /\ l' = l + 1
    /\ TLCSet(0, Max({l', TLCGet(0)}))

IsRwTxRequestAction ==
    /\ IsEvent("RwTxRequestAction")
    \* Model action
    /\ RwTxRequestAction
    \* Match message contents
    /\ Last(history').type = ToTxType[logline.type]
    /\ Last(history').tx = logline.tx

IsRwTxExecuteAction ==
    /\ IsEvent("RwTxExecuteAction")
    \* RwTxExecuteAction can only take place if a branch exists for the view
    \* If there is no branch, BackfillLedgerBranches will create the right amount of branches
    /\ Len(ledgerBranches) >= logline.tx_id[1]
    \* That branch contains just the right amount of transactions (seqno - 1)
    \* If that's not the case, BackfillLedgerBranche will create the right amount of txs
    /\ Len(ledgerBranches[logline.tx_id[1]]) = logline.tx_id[2] - 1
    \* Model action
    /\ RwTxExecuteAction
    \* Match message contents
    /\ Last(history').tx = logline.tx

IsRwTxResponseAction ==
    /\ IsEvent("RwTxResponseAction")
    \* Model action
    /\ RwTxResponseAction
    \* Match message contents
    /\ Last(history').type = ToTxType[logline.type]
    /\ Last(history').tx = logline.tx
    /\ Last(history').tx_id = logline.tx_id

IsStatusCommittedResponseAction ==
    /\ IsEvent("StatusCommittedResponseAction")
    \* Model action
    /\ StatusCommittedResponseAction
    \* Match message contents
    /\ Last(history').type = ToTxType[logline.type]
    /\ Last(history').status = ToStatus[logline.status]
    /\ Last(history').tx_id = logline.tx_id

IsRoTxRequestAction ==
    /\ IsEvent("RoTxRequestAction")
    \* Model action
    /\ RoTxRequestAction
    \* Match message contents
    /\ Last(history').type = ToTxType[logline.type]
    /\ Last(history').tx = logline.tx

IsRoTxResponseAction ==
    /\ IsEvent("RoTxResponseAction")
    \* RoTxResponseAction can only take place if a branch exists for the view
    \* If there is no branch, BackfillLedgerBranches will create the right amount of branches
    /\ Len(ledgerBranches) >= logline.tx_id[1]
    \* That branch contains just the right amount of transactions (seqno)
    \* If that's not the case, BackfillLedgerBranch will create the right amount of txs
    /\ Len(ledgerBranches[logline.tx_id[1]]) = logline.tx_id[2]
    \* Model action
    /\ RoTxResponseAction
    \* Match message contents
    /\ Last(history').type = ToTxType[logline.type]
    /\ Last(history').tx = logline.tx

IsStatusInvalidResponseAction ==
    /\ IsEvent("StatusInvalidResponseAction")
    \* Model action
    /\ StatusInvalidResponseAction
    \* Match message contents
    /\ Last(history').type = ToTxType[logline.type]
    /\ Last(history').status = ToStatus[logline.status]
    /\ Last(history').tx_id = logline.tx_id

\* Matches an event, but without advancing the log line. Useful to apply changes
\* before an event can be handled, for example backfilling the ledger branch, or
\* creating new ledger branches.
PreEvent(e) ==
    /\ logline.action = e
    /\ l' = l
    /\ l \in 1..Len(JsonLog)

BackfillLedgerBranch(bound) ==
    /\ LET view == logline.tx_id[1]
       IN /\ Len(ledgerBranches) >= view
          /\ Len(ledgerBranches[view]) < bound
          /\ ledgerBranches' = [ledgerBranches EXCEPT ![view] = Append(@, [view |-> view])]
    /\ UNCHANGED history    

BackfillLedgerBranchForWrite ==
    \* Similar to AppendOtherTxnAction, but only append to the specific branch
    \* necessary to enable the next transaction to execute.
    /\ PreEvent("RwTxExecuteAction")
    /\ BackfillLedgerBranch(logline.tx_id[2] - 1)

BackfillLedgerBranchForRead ==
    \* Similar to AppendOtherTxnAction, but only append to the specific branch
    \* necessary to enable the next transaction to execute.
    /\ PreEvent("RoTxResponseAction")
    \* There is no separate RoTxExecuteAction, but conceptually,
    \* we would backfill before it as well. Instead we do before the
    \* RoTxResponseAction, which is the earliest possible opportunity.
    /\ BackfillLedgerBranch(logline.tx_id[2])

BackfillLedgerBranches ==
    /\
       \/ PreEvent("RwTxExecuteAction")
       \* There is no separate RoTxExecuteAction, but conceptually,
       \* we would backfill before it as well. Instead we do before the
       \* RoTxResponseAction, which is the earliest possible opportunity.
       \/ PreEvent("RoTxResponseAction")
    \* Similar to TruncateLedgerAction, but only advances the view
    /\ LET view == logline.tx_id[1]
           seqno == logline.tx_id[2]
       IN /\ Len(ledgerBranches) < view
          /\ ledgerBranches' = Append(ledgerBranches, Last(ledgerBranches))
    /\ UNCHANGED history

TraceNext ==
    \/ IsRwTxRequestAction
    \/ IsRwTxExecuteAction
    \/ IsRwTxResponseAction
    \/ IsStatusCommittedResponseAction
    \/ IsRoTxRequestAction
    \/ IsRoTxResponseAction
    \/ IsStatusInvalidResponseAction
    \/ BackfillLedgerBranchForRead
    \/ BackfillLedgerBranchForWrite
    \/ BackfillLedgerBranches

TraceSpec ==
    TraceInit /\ [][TraceNext]_<<l, vars>>

-------------------------------------------------------------------------------------

Termination ==
    l = Len(JsonLog) => TLCSet("exit", TRUE)

-------------------------------------------------------------------------------------

TraceMatched ==
    \* We force TLC to check TraceMatched as a temporal property because TLC checks temporal
    \* properties after generating all successor states of the current state, unlike
    \* invariants that are checked after generating a successor state.
    \* If the queue is empty after generating all successors of the current state,
    \* and l is less than the length of the trace, then TLC failed to validate the trace.
    \*
    \* Note: Consider strengthening (Nat \ {0}) to {1} when validating traces with no nondeterminism.
    [](l <= Len(JsonLog) => [](TLCGet("queue") \in Nat \ {0} \/ l > Len(JsonLog)))

TraceMatchedNonTrivially ==
    \* If, e.g., the FALSE state constraint excludes all states, TraceMatched won't be violated.
    TLCGet(0) >= Len(JsonLog)

MNR == INSTANCE MultiNodeReads

MNRSpec == MNR!SpecMultiNodeReads

-------------------------------------------------------------------------------------

\* Does not include backfilled transactions
ClientTxnsOnlyAlias ==
    [
        l |-> l,
        history |-> history,
        ledgerBranches |-> [ b \in DOMAIN ledgerBranches |-> [ e \in { i \in DOMAIN ledgerBranches[b] : "tx" \in DOMAIN ledgerBranches[b][i] } |-> ledgerBranches[b][e] ] ]
    ]
==================================================================================
